\batchmode
\makeatletter
\def\input@path{{/Users/sergei.winitzki/Code/talks/ftt-fp/}}
\makeatother
\documentclass[english]{beamer}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}
\usepackage{babel}
\usepackage{amsmath}
\ifx\hypersetup\undefined
  \AtBeginDocument{%
    \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
  }
\else
  \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
\fi

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
 % this default might be overridden by plain title style
 \newcommand\makebeamertitle{\frame{\maketitle}}%
 % (ERT) argument for the TOC
 \AtBeginDocument{%
   \let\origtableofcontents=\tableofcontents
   \def\tableofcontents{\@ifnextchar[{\origtableofcontents}{\gobbletableofcontents}}
   \def\gobbletableofcontents#1{\origtableofcontents}
 }
 \newenvironment{lyxcode}
   {\par\begin{list}{}{
     \setlength{\rightmargin}{\leftmargin}
     \setlength{\listparindent}{0pt}% needed for AMS classes
     \raggedright
     \setlength{\itemsep}{0pt}
     \setlength{\parsep}{0pt}
     \normalfont\ttfamily}%
    \def\{{\char`\{}
    \def\}{\char`\}}
    \def\textasciitilde{\char`\~}
    \item[]}
   {\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usetheme[secheader]{Boadilla}
\usecolortheme{seahorse}
\title[Chapter 4: Functors]{Chapter 4: Functors}
\subtitle{Their laws and structure}
\author{Sergei Winitzki}
\date{December 28, 2017}
\institute[ABTB]{Academy by the Bay}
\setbeamertemplate{navigation symbols}{}

\makeatother

\begin{document}
\frame{\titlepage}
\begin{frame}{``Container-like'' type constructors}

\begin{itemize}
\item Visualize \texttt{\textcolor{blue}{\footnotesize{}Seq{[}T{]}}} as
a container with some items of type \texttt{\textcolor{blue}{\footnotesize{}T}}{\footnotesize \par}
\begin{itemize}
\item How to formalize this idea as a property of \texttt{\textcolor{blue}{\footnotesize{}Seq}}?
\end{itemize}
\item Another example of a container: \texttt{\textcolor{blue}{\footnotesize{}Future{[}T{]}}}{\footnotesize \par}
\begin{itemize}
\item a value of type \texttt{\textcolor{blue}{\footnotesize{}T}} will be
available later, or may fail to arrive
\end{itemize}
\end{itemize}
Let us separate the ``bare container'' functionality from other
functionality
\begin{itemize}
\item A ``bare container'' will allow us to:
\begin{itemize}
\item manipulate items held within the container
\begin{itemize}
\item In FP, to ``manipulate items'' means to \emph{apply functions to
values}
\end{itemize}
\end{itemize}
\item ``Container holds items'' = we can apply a function to the items
\begin{itemize}
\item but the new items \emph{remain} within the same container!
\item need \texttt{\textcolor{blue}{\footnotesize{}map{[}A,B{]}:\ Container{[}A{]}
$\Rightarrow$ (A $\Rightarrow$ B) $\Rightarrow$ Container{[}B{]}}}{\footnotesize \par}
\end{itemize}
\item A ``bare container'' will \emph{not} allow us to:
\begin{itemize}
\item make a new container out of a given set of items
\item read values out of the container
\item add more items into container, or delete items from container
\item wait and get notified when new items become available in container
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{\texttt{Option{[}T{]}} as a container I}

\begin{itemize}
\item In the short notation: $\text{Option}^{A}=1+A$
\item The \texttt{\textcolor{blue}{\footnotesize{}map}} function is required
to have the type
\[
\text{map}^{A,B}:1+A\Rightarrow\left(A\Rightarrow B\right)\Rightarrow1+B
\]
\item This function produces a new $\text{Option}^{B}$ value, possibly
containing transformed data
\end{itemize}
Main questions:
\begin{enumerate}
\item How to avoid ``information loss'' in this function?
\item Does this \texttt{\textcolor{blue}{\footnotesize{}map}} allow us to
``manipulate values within the container''?
\end{enumerate}
\end{frame}

\begin{frame}{\texttt{Option{[}T{]}} as a container II}

Avoiding ``information loss'' means:
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}map{[}A,A{]}(opt)(x$\Rightarrow$x)
== opt}} \textendash{} ``\textbf{identity law}'' for \texttt{\textcolor{blue}{\footnotesize{}map}}{\footnotesize \par}
\item Actually, we have two implementations of the type: 
\[
\text{map}^{[A,B]}=(1+a^{A})\Rightarrow(f^{A\Rightarrow B})\Rightarrow1+f(a)
\]
and
\[
\text{map}^{[A,B]}=(1+a^{A})\Rightarrow(f^{A\Rightarrow B})\Rightarrow1+0^{B}
\]
The second implementation has ``information loss''!
\item Short notation for code (type annotations are optional):
\end{itemize}
\begin{center}
\begin{tabular}{|c|c|}
\hline 
\textbf{Short notation} &
\textbf{Scala code}\tabularnewline
\hline 
\hline 
$a^{A}$ &
\texttt{\textcolor{blue}{\footnotesize{}val a: A}}\tabularnewline
\hline 
$f^{[A]\,B\Rightarrow C}=...$ &
\texttt{\textcolor{blue}{\footnotesize{}def f{[}A{]}: B $\Rightarrow$
C = \{...\}}}\tabularnewline
\hline 
$(a^{A}+b^{B})\Rightarrow...$ &
\texttt{\textcolor{blue}{\footnotesize{}x: Either{[}A, B{]} match
\{...\}}}\tabularnewline
\hline 
$a^{A}+0^{B}$ &
\texttt{\textcolor{blue}{\footnotesize{}Left(a):\ Either{[}A, B{]}}}\tabularnewline
\hline 
$1$ &
\texttt{\textcolor{blue}{\footnotesize{}()}}, also \texttt{\textcolor{blue}{\footnotesize{}None}}\tabularnewline
\hline 
\end{tabular}
\par\end{center}

\end{frame}

\begin{frame}{\texttt{Option{[}T{]}} as a container III}


\framesubtitle{What it means to ``be able to manipulate values in a container''}
\begin{itemize}
\item Flip the two curried arguments in the type signature of \texttt{\textcolor{blue}{\footnotesize{}map}}:{\footnotesize{}
\[
\text{fmap}^{[A,B]}:\left(A\Rightarrow B\right)\Rightarrow\text{Option}^{A}\Rightarrow\text{Option}^{B}
\]
}{\footnotesize \par}
\item A function $f$ is ``\textbf{lifted}'' from $A\Rightarrow B$ to
$\text{Option}^{A}\Rightarrow\text{Option}^{B}$ by \texttt{\textcolor{blue}{\footnotesize{}fmap}}:{\footnotesize{}
\[
\text{fmap}(f^{A\Rightarrow B}):\text{Option}^{A}\Rightarrow\text{Option}^{B}
\]
}{\footnotesize \par}
\item Being able to manipulate values means that functions \emph{behave
normally when lifted}, i.e.\ when applied within the container
\item The standard properties of function composition are{\footnotesize{}
\begin{align*}
f^{A\Rightarrow B}\circ id^{B\Rightarrow B} & =f^{A\Rightarrow B}\\
id^{A\Rightarrow A}\circ f^{A\Rightarrow B} & =f^{A\Rightarrow B}\\
f^{A\Rightarrow B}\circ(g^{B\Rightarrow C}\circ h^{C\Rightarrow D}) & =(f^{A\Rightarrow B}\circ g^{B\Rightarrow C})\circ h^{C\Rightarrow D}
\end{align*}
}and should hold for the ``lifted'' functions as well!
\item The ``identity law'' already requires that {\footnotesize{}$\text{fmap}(\text{id}^{A\Rightarrow A})=\text{id}^{\text{Option}^{A}\Rightarrow\text{Option}^{A}}$}{\footnotesize \par}
\item It remains to require that \texttt{\textcolor{blue}{\footnotesize{}fmap}}
should preserve function composition:{\footnotesize{}
\[
\text{fmap}(f^{A\Rightarrow B}\circ g^{B\Rightarrow C})=\text{fmap}(f^{A\Rightarrow B})\circ\text{fmap}(g^{B\Rightarrow C})
\]
}{\footnotesize \par}
\end{itemize}
\end{frame}

\begin{frame}{Functor: the definition}


\framesubtitle{An abstraction for the functionality of a ``bare container'' }

A \textbf{functor} is:
\begin{itemize}
\item a data type having a type parameter, e.g.\ \texttt{\textcolor{blue}{\footnotesize{}MyData{[}T{]}}}{\footnotesize \par}
\item such that a function \texttt{\textcolor{blue}{\footnotesize{}map}}
or, equivalently, \texttt{\textcolor{blue}{\footnotesize{}fmap}} is
available:{\footnotesize{}
\begin{align*}
\text{map}^{[A,B]}:\  & \text{MyData}^{A}\Rightarrow\left(A\Rightarrow B\right)\Rightarrow\text{MyData}^{B}\\
\text{fmap}^{[A,B]}: & \left(A\Rightarrow B\right)\Rightarrow\text{MyData}^{A}\Rightarrow\text{MyData}^{B}
\end{align*}
}{\footnotesize \par}
\item such that the identity law and the composition law hold
\begin{itemize}
\item The laws are easier to formulate in terms of \texttt{\textcolor{blue}{\footnotesize{}fmap}}:\texttt{\textcolor{blue}{\footnotesize{}
\begin{align*}
\text{fmap}^{A,A}\,(\text{id}^{A\Rightarrow A}) & =\text{id}^{F^{A}\Rightarrow F^{A}}\\
\text{fmap}(f^{A\Rightarrow B}\circ g^{B\Rightarrow C}) & =\text{fmap}(f^{A\Rightarrow B})\circ\text{fmap}(g^{B\Rightarrow C})
\end{align*}
}}{\footnotesize \par}
\end{itemize}
\item Verify the laws for \texttt{\textcolor{blue}{\footnotesize{}Option{[}A{]}}}:
see test code
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~fmap{[}A,B{]}(f:~(A~$\Rightarrow$~B)):~Option{[}A{]}~$\Rightarrow$~Option{[}B{]}~=~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~case~Some(x)~$\Rightarrow$~Some(f(x))}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~case~None~$\Rightarrow$~None}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}}{\footnotesize \par}
\end{lyxcode}
\end{frame}

\begin{frame}{Examples of functors I}


\framesubtitle{(Almost) everything that has a ``\texttt{map}'' is a functor}
\begin{itemize}
\item Specific functors will have methods for creating them, reading values
out of them, adding / removing items, waiting for items to arrive,
etc.
\begin{itemize}
\item Common to all functors is the \texttt{\textcolor{blue}{\footnotesize{}map}}
function
\item Right now we are only concerned about the properties of \texttt{\textcolor{blue}{\footnotesize{}map}}{\footnotesize \par}
\end{itemize}
\end{itemize}
Examples of functors in the Scala standard library:
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}Option{[}T{]}}}{\footnotesize \par}
\item \texttt{\textcolor{blue}{\footnotesize{}Either{[}L, R{]}}} with respect
to \texttt{\textcolor{blue}{\footnotesize{}R}}{\footnotesize \par}
\item \texttt{\textcolor{blue}{\footnotesize{}Seq{[}T{]}}} and \texttt{\textcolor{blue}{\footnotesize{}Iterator{[}T{]} }}{\footnotesize \par}
\item various subtypes of \texttt{\textcolor{blue}{\footnotesize{}Seq}}
(\texttt{\textcolor{blue}{\footnotesize{}Range}}, \texttt{\textcolor{blue}{\footnotesize{}List}},
\texttt{\textcolor{blue}{\footnotesize{}Vector}}, \texttt{\textcolor{blue}{\footnotesize{}IndexedSeq}},
etc.)
\item \texttt{\textcolor{blue}{\footnotesize{}Future{[}T{]}}}, \texttt{\textcolor{blue}{\footnotesize{}Try{[}T{]}}}{\footnotesize \par}
\item \texttt{\textcolor{blue}{\footnotesize{}Map{[}K, V{]}}} with respect
to \texttt{\textcolor{blue}{\footnotesize{}V}} (using \texttt{\textcolor{blue}{\footnotesize{}mapValues}})
\end{itemize}
Examples of \emph{not-really-functors} that have a \texttt{\textcolor{blue}{\footnotesize{}map}}:
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}Set{[}T{]}}} \textendash{}
it works only when \texttt{\textcolor{blue}{\footnotesize{}T}} has
a well-behaved ``\texttt{\textcolor{blue}{\footnotesize{}==}}''
operation
\item \texttt{\textcolor{blue}{\footnotesize{}Map{[}K, V{]}}} with respect
to both \texttt{\textcolor{blue}{\footnotesize{}K}} and \texttt{\textcolor{blue}{\footnotesize{}V}},
because it is a \texttt{\textcolor{blue}{\footnotesize{}Set}} w.r.t.
\texttt{\textcolor{blue}{\footnotesize{}K}}{\footnotesize \par}
\item See test code
\end{itemize}
\end{frame}

\begin{frame}{Examples of functors II}


\framesubtitle{Polynomial type constructors as functors}
\begin{enumerate}
\item Short notation: $\text{QueryResult}^{A}=\text{String}\times\text{Int}\times A$
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}case~class~QueryResult{[}A{]}(name:~String,~time:~Int,~data:~A)}{\footnotesize \par}
\end{lyxcode}
\item Short notation: $\text{Vec3}^{A}=A\times A\times A$
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}case~class~Vec3{[}A{]}(x:~A,~y:~A,~z:~A)}{\footnotesize \par}
\end{lyxcode}
\item Short notation: $\text{QueryResult}^{A}=\text{String}+\text{String}\times\text{Int}\times A$
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~QueryResult{[}A{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~Error{[}A{]}(message:~String)~extends~QueryResult{[}A{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~Success{[}A{]}(name:~String,~time:~Int,~data:~A)~}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~~~~~~~~~~~~~~~~~~extends~QueryResult{[}A{]}}{\footnotesize \par}
\end{lyxcode}
\end{enumerate}
See test code
\end{frame}

\begin{frame}{Examples of functors III: non-functors I}


\framesubtitle{Data types that cannot have ``\texttt{map}'' at all, due to type
problems}
\begin{enumerate}
\item Data types that \emph{consume} a value of the parameter type
\[
\text{NotContainer}^{A}=\left(A\Rightarrow\text{Int}\right)\times A
\]

\begin{lyxcode}
\textcolor{blue}{\footnotesize{}case~class~NotContainer{[}A{]}(x:~A~$\Rightarrow$~Int,~y:~A)}{\footnotesize \par}
\end{lyxcode}
\item Disjunction types with non-parametric type values
\end{enumerate}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~ServerAction{[}Res{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~GetResult{[}Res{]}(r:~Long~$\Rightarrow$~Res)~extends~ServerAction{[}Res{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~StoreId(x:~Long,~y:~String)~extends~ServerAction{[}Long{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~StoreName(name:~String)~extends~ServerAction{[}String{]}}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item The type \texttt{\textcolor{blue}{\footnotesize{}ServerAction{[}Res{]}}}
is called a GADT (``generalized algebraic data type'')
\begin{itemize}
\item Not sure what the short notation should be for GADTs!
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Examples of functors III: non-functors II}


\framesubtitle{These \emph{could} be functors, except for incorrect implementations
of ``\texttt{map}''}

We need a well-behaved $\text{fmap}\,(f^{A\Rightarrow B}):\text{Container}^{A}\Rightarrow\text{Container}^{B}$

What could go wrong?
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}fmap(f)}} ignores \texttt{\textcolor{blue}{\footnotesize{}f}}
\textendash{} e.g.\ always returns \texttt{\textcolor{blue}{\footnotesize{}None}}
for \texttt{\textcolor{blue}{\footnotesize{}Option{[}B{]}}}{\footnotesize \par}
\item \texttt{\textcolor{blue}{\footnotesize{}fmap(f)}} reorders data items
in a container: 
\[
\text{Container}^{A}\equiv A\times A;\qquad\text{fmap}^{A,B}\,(f^{A\Rightarrow B})({\color{blue}x}^{A},{\color{blue}y}^{A})=\left(f({\color{blue}y}),f({\color{blue}x})\right)
\]
e.g.\ swaps some elements in $A\times A\times A$:
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~fmap{[}A,~B{]}(f:~A~$\Rightarrow$~B):~Vec3{[}A{]}~$\Rightarrow$~Vec3{[}B{]}~=}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~\{~case~Vec3(x,~y,~z)~$\Rightarrow$~Vec3(f(y),~f(x),~f(z))~\}}{\footnotesize \par}
\end{lyxcode}
\item Does a special computation if types are equal: if \texttt{\textcolor{blue}{\footnotesize{}A}}
and \texttt{\textcolor{blue}{\footnotesize{}B}} are the same type,
do \texttt{\textcolor{blue}{\footnotesize{}fmap{[}A, A{]}(f) = identity}},
otherwise $f(x)$ is applied
\item Does a special computation if type is equal to a specific type, e.g.\ if
\texttt{\textcolor{blue}{\footnotesize{}A = B = Int}} then do $f(f(x))$
else $f(x)$
\item Does a special computation if $f$ is equal to some $f_{0}$, otherwise
use $f(x)$
\end{itemize}
See test code
\end{frame}

\begin{frame}{Recursive polynomial types as functors}

\begin{itemize}
\item Example: List of even length is a recursive type,
\begin{align*}
LP^{A} & \equiv1+A\times A\times LP^{A}\\
 & =1+A\times A+A\times A\times A\times A+...
\end{align*}
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~LP{[}A{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}final~case~class~LPempty{[}A{]}()~extends~LP{[}A{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}final~case~class~LPpair{[}A{]}(x:~A,~y:~A,~tail:~LP{[}A{]})~extends~LP{[}A{]}}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item We can implement \texttt{\textcolor{blue}{\footnotesize{}fmap}} as
a recursive function:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~fmap{[}A,~B{]}(f:~A~$\Rightarrow$~B):~LP{[}A{]}~$\Rightarrow$~LP{[}B{]}~=~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~case~LPempty()~$\Rightarrow$~LPempty{[}B{]}()}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~case~LPpair(x,~y,~tail)~$\Rightarrow$~LPpair{[}B{]}(f(x),~f(y),~fmap(f)(tail))}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item This is the only way to implement \texttt{\textcolor{blue}{\footnotesize{}fmap}}
that satisfies the functor laws!
\end{itemize}
See test code for checking the functor laws
\end{frame}

\begin{frame}{Contrafunctors}

\begin{itemize}
\item The type  $C^{A}\equiv A\Rightarrow\text{Int}$ is not a functor (impossible
to implement \texttt{\textcolor{blue}{\footnotesize{}map}}), but we
can implement \texttt{\textcolor{blue}{\footnotesize{}contrafmap}}:
\[
\text{contrafmap}^{A,B}:\left({\color{blue}B\Rightarrow A}\right)\Rightarrow C^{A}\Rightarrow C^{B}
\]
\item The contrafunctor laws are analogous to functor laws:\texttt{\textcolor{blue}{\footnotesize{}
\begin{align*}
\text{contrafmap}^{A,A}(\text{id}^{A\Rightarrow A}) & =\text{id}^{C^{A}\Rightarrow C^{A}}\\
\text{contrafmap}\left(g\circ f\right) & =\text{contrafmap}\left(f\right)\circ\text{contrafmap}\left(g\right)
\end{align*}
}}The ``contra-'' reverses the arrow between $A$ and $B$
\item The type parameter $A$ is to the left of the function arrow (``consumed'')
\item ``Functors contain data; contrafunctors consume data''
\end{itemize}
Example of non-contrafunctor:
\begin{itemize}
\item The type $\text{NotContainer}^{A}=\left(A\Rightarrow\text{Int}\right)\times A$
is neither a functor nor a contrafunctor
\end{itemize}
\end{frame}

\begin{frame}{Covariance, contravariance, and subtyping}

\begin{itemize}
\item Example of subtyping:
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~AtMostTwo}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}final~case~class~Zero()~extends~AtMostTwo}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}final~case~class~One(x:~Int)~extends~AtMostTwo}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}final~case~class~Two(x:~Int,~y:~Int)~extends~AtMostTwo}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item Here \texttt{\textcolor{blue}{\footnotesize{}Zero}}, \texttt{\textcolor{blue}{\footnotesize{}One}},
and \texttt{\textcolor{blue}{\footnotesize{}Two}} are \textbf{subtypes}
of \texttt{\textcolor{blue}{\footnotesize{}AtMostTwo}}{\footnotesize \par}
\end{itemize}
\item We can pass \texttt{\textcolor{blue}{\footnotesize{}Two(10, 20)}}
to a function that takes an \texttt{\textcolor{blue}{\footnotesize{}AtMostTwo}}{\footnotesize \par}
\item This is equivalent to an automatic type conversion \texttt{\textcolor{blue}{\footnotesize{}Two
$\Rightarrow$ AtMostTwo}}{\footnotesize \par}
\item A container \texttt{\textcolor{blue}{\footnotesize{}C{[}A{]}}} is
\textbf{covariant} if \texttt{\textcolor{blue}{\footnotesize{}C{[}Two{]}}}
is a subtype of \texttt{\textcolor{blue}{\footnotesize{}C{[}AtMostTwo{]}}}{\footnotesize \par}
\begin{itemize}
\item And then a type conversion function\texttt{\textcolor{blue}{\footnotesize{}
C{[}Two{]} $\Rightarrow$ C{[}AtMostTwo{]}}} exists
\end{itemize}
\item More generally, when \texttt{\textcolor{blue}{\footnotesize{}X}} is
a subtype of \texttt{\textcolor{blue}{\footnotesize{}Y}} then we have
\texttt{\textcolor{blue}{\footnotesize{}X $\Rightarrow$ Y}} and we
need \texttt{\textcolor{blue}{\footnotesize{}C{[}X{]} $\Rightarrow$
C{[}Y{]}}}, which is guaranteed if we have a function of typeed if we have a function of type
\[
\left(X\Rightarrow Y\right)\Rightarrow(C^{X}\Rightarrow C^{Y})
\]
\item Scala supports covariance annotations on types: \texttt{\textcolor{blue}{\footnotesize{}sealed
trait C{[}+T{]}}}{\footnotesize \par}
\end{itemize}
Functors are covariant, contrafunctors are contravariant
\end{frame}

\begin{frame}{Worked examples I}

\begin{itemize}
\item Decide if a data type is a functor, a contrafunctor, or neither
\item Implement a \texttt{\textcolor{blue}{\footnotesize{}fmap}} or a \texttt{\textcolor{blue}{\footnotesize{}contrafmap}}
function that satisfies the laws
\end{itemize}
\begin{enumerate}
\item Define case classes for these types, and implement \texttt{\textcolor{blue}{\footnotesize{}fmap}}:
\begin{enumerate}
\item $\text{Data}^{A}\equiv\text{String}+A\times\text{Int}+A\times A\times A$
\item $\text{Data}^{A}\equiv1+A\times(\text{Int}\times\text{String}+A)$
\item $\text{Data}^{A}\equiv\left(\text{String}\Rightarrow\text{Int}\Rightarrow A\right)\times A+\left(\text{Boolean}\Rightarrow\text{Double}\Rightarrow A\right)\times A$
\end{enumerate}
\item Decide which of these types are functors or contrafunctors, and implement
\texttt{\textcolor{blue}{\footnotesize{}fmap}} or \texttt{\textcolor{blue}{\footnotesize{}contrafmap}}
respectively:
\begin{enumerate}
\item $\text{Data}^{A}\equiv\left(A\Rightarrow\text{Int}\right)+\left(A\Rightarrow A\Rightarrow\text{String}\right)$
\item $\text{Data}^{A,B}\equiv\left(A+B\right)\times\left(\left(A\Rightarrow\text{Int}\right)\Rightarrow B\right)$
\end{enumerate}
\item Rewrite this code in the short notation; identify covariant and contravariant
type usages; verify that with covariance annotations:
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~Coi{[}A,~B{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~Pa{[}A,~B{]}(b:~(A,~B),~c:~B$\Rightarrow$Int)~~extends~Coi{[}A,~B{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~Re{[}A,~B{]}(d:~A,~e:~B,~c:~Int)~~~~extends~Coi{[}A,~B{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~Ci{[}A,~B{]}(f:~String$\Rightarrow$A,~g:~B$\Rightarrow$A)~extends~Coi{[}A,~B{]}}{\footnotesize \par}
\end{lyxcode}
\end{enumerate}
\end{frame}

\begin{frame}{Exercises I}

Define case classes for these types, decide if they are covariant
or contravariant, and implement \texttt{\textcolor{blue}{\footnotesize{}fmap}}
or \texttt{\textcolor{blue}{\footnotesize{}contrafmap}} as needed:
\begin{enumerate}
\item $\text{Data}^{A}\equiv\left(1+A\right)\times\left(1+A\right)\times\text{String}$
\item $\text{Data}^{A}\equiv\left(A\Rightarrow\text{String}\right)\Rightarrow\left(A\times\left(\text{Int}+A\right)\right)$
\item $\text{Data}^{A,B}\equiv\left(A\Rightarrow\text{String}\right)\times\left(\left(A+B\right)\Rightarrow\text{Int}\right)$
\item $\text{Data}^{A}\equiv\left(1+\left(A\Rightarrow\text{String}\right)\right)\Rightarrow\left(1+\left(A\Rightarrow\text{Int}\right)\right)\Rightarrow\text{Int}$
\item $\text{Data}^{B}\equiv\left(B+\left(\text{Int}\Rightarrow B\right)\right)\times\left(B+\left(\text{String}\Rightarrow B\right)\right)$
\item Rewrite this code in the short notation; identify covariant and contravariant
type usages; verify that with covariance annotations:
\end{enumerate}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~Result{[}A,B{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~P{[}A,B{]}(a:~A,~b:~B,~c:~Int)~~~extends~Result{[}A,B{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~Q{[}A,B{]}(d:~Int$\Rightarrow$A,~e:~Int$\Rightarrow$B)~extends~Result{[}A,B{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}case~class~R{[}A,B{]}(f:~A$\Rightarrow$A,~g:~A$\Rightarrow$B)~~~~~extends~Result{[}A,B{]}}{\footnotesize \par}
\end{lyxcode}
\end{frame}

\begin{frame}{The structure of functor types I}

\framesubtitle{How to build new functors out of old ones}

Main question:
\begin{itemize}
\item Is any data type $Z^{A}$ with $A$ in covariant positions always
a functor? {\footnotesize{}
\[
Z^{A,R}\equiv\left(\left(A\Rightarrow R\right)\Rightarrow R\right)\times A+\left(R\Rightarrow A+\text{Int}\right)+A\times A\times\text{Int}\times\text{Int}
\]
}{\footnotesize \par}
\item ``Elementary'' data types are built from parts:
\begin{itemize}
\item Constant types $1$, $\text{Int}$, $\text{String}$, etc.
\item Type parameters $A$, $B$, ..., $Z$, etc.
\item Previously defined type constructors $F^{A}$, $G^{A}$, etc.
\item Four operations: $F^{A}+G^{A}$,\  $F^{A}\times G^{A}$,\  $F^{A}\Rightarrow G^{A}$,\ 
$F^{G^{A}}$ (composition)
\item Each time a type $A$ is moved to the left of $\Rightarrow$, its
covariance is reversed
\begin{itemize}
\item So $A\Rightarrow Z$ is contravariant in $A$, but $\left(A\Rightarrow Z\right)\Rightarrow Z$
is again covariant
\end{itemize}
\item If we exclude the operation $F^{A}\Rightarrow G^{A}$, the result
is always covariant
\begin{itemize}
\item This yields polynomial type constructors = \textbf{polynomial functors}
\end{itemize}
\end{itemize}
\end{itemize}
To answer the question:
\begin{itemize}
\item Build \texttt{\textcolor{blue}{\footnotesize{}fmap}} incrementally
as we build up the type expression
\item Verify that the laws hold at every step
\end{itemize}
\end{frame}

\begin{frame}{The structure of functor types II}

\framesubtitle{The building blocks}
\begin{itemize}
\item Building blocks: creating functors from scratch
\begin{itemize}
\item \textbf{Constant} functors $\text{Const}^{C,A}\equiv C$ with $\text{fmap}(f)=id$,
and are at the same time contrafunctors with $\text{contrafmap}(f)=id$
\item \textbf{Identity} functor $\text{Id}^{A}=A$ with $\text{fmap}(f)=f$
(not a contrafunctor!)
\end{itemize}
\item Operations: creating new functors out of previous ones
\begin{itemize}
\item In each case, we already have the \texttt{\textcolor{blue}{\footnotesize{}fmap}}
implementations for $F^{A}$ and $G^{A}$, and we assume that their
functor laws were already checked 
\item $F^{A}+G^{A}$ \textendash{} \texttt{\textcolor{blue}{\footnotesize{}fmap}}
is built by pattern-matching and preserving the sides
\item $F^{A}\times G^{A}$ \textendash{} \texttt{\textcolor{blue}{\footnotesize{}fmap}}
is built by tupling the two \texttt{\textcolor{blue}{\footnotesize{}fmap}}
results, in order
\item $F^{A}\Rightarrow G^{A}$ \textendash{} \texttt{\textcolor{blue}{\footnotesize{}fmap}}
is built by substituting the function argument
\begin{itemize}
\item Here $F^{A}$ must be a contrafunctor and $G^{A}$ must be a functor
\end{itemize}
\item $F^{G^{A}}$ (\texttt{\textcolor{blue}{\footnotesize{}F{[}G{[}A{]}{]}}}
in code) \textendash{} \texttt{\textcolor{blue}{\footnotesize{}fmap}}
is built by composing the two \texttt{\textcolor{blue}{\footnotesize{}fmap}}s
\item Type recursion: $F^{A}=R^{A,F^{A}}$, where $R^{A,X}$ is a functor
in $A$ and $X$
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}fmap}} for $F^{A}$ is recursive,
uses the two \texttt{\textcolor{blue}{\footnotesize{}fmap}}s of $R^{A,X}$
\end{itemize}
\end{itemize}
\item Similar constructions hold for contrafunctors, \emph{mutatis mutandis}
\end{itemize}
Will now check that the functor laws still hold after each operation
\end{frame}

\begin{frame}{Worked examples II: Checking the functor laws}

To check that the \texttt{\textcolor{blue}{\footnotesize{}fmap}} laws
hold for $F^{A}+G^{A}$ if they hold for $F^{A}$ and $G^{A}$
\begin{itemize}
\item From $f:A\Rightarrow B$, get $\text{fmap}_{F}(f):F^{A}\Rightarrow F^{B}$
and $\text{fmap}_{G}(f):G^{A}\Rightarrow G^{B}$
\item Define $\text{fmap}_{F+G}(f)=(p^{F^{A}}+q^{G^{A}})\Rightarrow\text{fmap}_{F}(f)(p)+\text{fmap}_{G}(f)(q)$
\item Identity law: $f=id$, so $\text{fmap}_{F}(f)=id$ and $\text{fmap}_{G}(f)=id$
\begin{itemize}
\item Hence we get $\text{fmap}_{F+G}(id)(p+q)=id(p)+id(q)=p+q$
\end{itemize}
\item Composition law: 
\begin{align*}
 & (\text{fmap}_{F+G}(f_{1})\circ\text{fmap}_{F+G}(f_{2}))(p+q)\\
=\  & \text{fmap}_{F+G}(f_{2})\left(\text{fmap}_{F}(f_{1})(p)+\text{fmap}_{G}(f_{1})(q)\right)\\
=\  & (\text{fmap}_{F}(f_{1})\circ\text{fmap}_{F}(f_{2}))(p)+\left(\text{fmap}_{G}(f_{1})\circ\text{fmap}_{G}(f_{2})\right)(q)\\
=\  & \text{fmap}_{F}(f_{1}\circ f_{2})(p)+\text{fmap}_{G}(f_{1}\circ f_{2})(q)\\
=\  & \text{fmap}_{F+G}(f_{1}\circ f_{2})(p+q)
\end{align*}
\item Note how $\text{fmap}_{F+G}(f)$ works on each side of $\left(p+q\right)$
separately
\item The laws would not hold if we mixed up some parts of $p$ and $q$
\end{itemize}
\end{frame}

\begin{frame}{Worked examples III: Checking the functor laws}

To show that $F^{A}\Rightarrow G^{A}$ is a functor, assuming that
$F^{A}$ is a contrafunctor and $G^{A}$ is a functor
\begin{itemize}
\item For a given $f:A\Rightarrow B$, denote for brevity $\gamma_{f}=\text{fmap}_{G}(f):G^{A}\Rightarrow G^{B}$
and $\phi_{f}=\text{contrafmap}_{F}(f):F^{B}\Rightarrow F^{A}$ ,
then define $\text{fmap}_{F\Rightarrow G}(f)(p:F^{A}\Rightarrow G^{A}):\left(F^{B}\Rightarrow G^{B}\right)=q\Rightarrow\gamma_{f}(p(\phi_{f}(q)))$
\item Identity law: $f=id$, so $\gamma_{f}=id$ and $\phi_{f}=id$
\begin{itemize}
\item Hence we get $\text{fmap}_{F\Rightarrow G}(id)(p^{F^{A}\Rightarrow G^{A}})=\left(q^{F^{A}}\Rightarrow p(q)\right)=p$
\end{itemize}
\item Composition law, assuming $\gamma_{f_{1}}\circ\gamma_{f_{2}}=\gamma_{f_{1}\circ f_{2}}$
and $\phi_{f_{2}}\circ\phi_{f_{1}}=\phi_{f_{1}\circ f_{2}}$: 
\begin{align*}
 & (\text{fmap}_{F\Rightarrow G}(f_{1})\circ\text{fmap}_{F\Rightarrow G}(f_{2}))(p^{F^{A}\Rightarrow G^{A}})\\
=\  & \text{fmap}_{F\Rightarrow G}(f_{2})\left(q\Rightarrow\gamma_{f_{1}}(p(\phi_{f_{1}}(q)))\right)\\
=\  & q\Rightarrow\gamma_{f_{2}}(\gamma_{f_{1}}(p(\phi_{f_{1}}(\phi_{f_{2}}(q)))))\\
=\  & q\Rightarrow\gamma_{f_{1}\circ f_{2}}(p(\phi_{f_{1}\circ f_{2}}(q)))\\
=\  & \text{fmap}_{F\Rightarrow G}(f_{1}\circ f_{2})(p)
\end{align*}
\item The order is reversed for $\phi$, so this wouldn't work if $F$ were
a functor
\end{itemize}
\end{frame}

\begin{frame}{Exercises II}
\begin{enumerate}
\item Check that the \texttt{\textcolor{blue}{\footnotesize{}fmap}} laws
hold for $F^{A}\times G^{A}$ if they hold for $F^{A}$ and $G^{A}$
\item Show that $F^{A}\Rightarrow G^{A}$ is, in general, neither a functor
nor a contrafunctor when both $F^{A}$ and $G^{A}$ are functors or
both are contrafunctors (an example of suitable $F^{A}$ and $G^{A}$
will be sufficient)
\item Show that $F^{A}\Rightarrow G^{A}$ is a contrafunctor if $F^{A}$
is a functor and $G^{A}$ is a contrafunctor, by checking the \texttt{\textcolor{blue}{\footnotesize{}contrafmap}}
laws for $F^{A}\Rightarrow G^{A}$ 
\end{enumerate}
\end{frame}

\end{document}
